$\forall$$T_{1}$, $T_{2}$:Type, ${\it as}$:($T_{1}$$\times$$T_{2}$) List. unzip(${\it as}$) $\in$ ($T_{1}$ List)$\times$($T_{2}$ List)